the_w:World, e, e':E. e = e'   

latex

Definitions	x:A. B(x), E, t  T, p = q, x. t(x), , x(s),
Lemmas	band wf, eq id wf, pi1 wf, Id wf, nat wf, eq int wf, pi2 wf, not wf, assert wf, w-isnull wf, w-a wf, world wf